<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>ProofConstants</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="ProofConstants";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/NullsPermittedRule.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/verify/ProofDerivationStepEntry.html" title="class in mmj.verify"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/ProofConstants.html" target="_top">Frames</a></li>
<li><a href="ProofConstants.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#methods_inherited_from_class_java.lang.Object">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li>Method</li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.verify</div>
<h2 title="Class ProofConstants" class="title">Class ProofConstants</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.verify.ProofConstants</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">ProofConstants</span>
extends java.lang.Object</pre>
<div class="block">Constants used in mmj.verify.VerifyProofs class.
 <p>
 VerifyProofs uses fixed size arrays that are reused from one proof to the
 next. This is much faster than reallocating everything for each proof, but it
 means that each instance of VerifyProofs requires massive storage and can
 only work on one proof at a time. It also means that Metamath databases like
 set.mm can overflow the arrays (set.mm is unbelievable!) Therefore,
 VerifyProofs dynamically reallocates its array after an overflow, up to a
 point; it throws an exception if a predetermined maximum size is exceeded,
 based on the idea that a bug in the code is more likely than a work formula
 having 32,000 symbols. The numbers can be changed here, in ProofConstants, up
 or down (have fun :).
 <hr>
 There are two primary types of constants: parameters that are "hardcoded"
 which affect/control processing, and error/info messages.
 <p>
 Each mmj message begins with a code, such as this:
 <p>
 <code>E-LA-0007</code>
 <p>
 where the format of the code is <code>X-YY-9999</code>
 <p>
 <b><code>X</code></b> : error level
 <ul>
 <li><code>E</code> = Error
 <li><code>I</code> = Information
 <li><code>A</code> = Abort (processing terminates, usually a bug).
 </ul>
 <p>
 <b><code>YY</code></b> : source code
 <ul>
 <li><code>GM</code> = mmj.gmff package (see <a href="../../mmj/gmff/GMFFConstants.html" title="class in mmj.gmff"><code>GMFFConstants</code></a>)
 <li><code>GR</code> = mmj.verify.Grammar and related code (see
 <a href="../../mmj/verify/GrammarConstants.html" title="class in mmj.verify"><code>GrammarConstants</code></a>)
 <li><code>IO</code> = mmj.mmio package (see <a href="../../mmj/mmio/MMIOConstants.html" title="class in mmj.mmio"><code>MMIOConstants</code></a>)
 <li><code>LA</code> = mmj.lang package (see <a href="../../mmj/gmff/GMFFConstants.html" title="class in mmj.gmff"><code>GMFFConstants</code></a>)
 <li><code>PA</code> = mmj.pa package (proof assistant) (see <a href="../../mmj/pa/PaConstants.html" title="class in mmj.pa"><code>PaConstants</code></a>)
 <li><code>PR</code> = mmj.verify.VerifyProof and related code (see
 <a href="../../mmj/verify/ProofConstants.html" title="class in mmj.verify"><code>ProofConstants</code></a>)
 <li><code>TL</code> = mmj.tl package (Theorem Loader).
 <li><code>TM</code> = mmj.tmff.AlignColumn and related code
 <li><code>UT</code> = mmj.util package. (see <a href="../../mmj/util/UtilConstants.html" title="class in mmj.util"><code>UtilConstants</code></a>)
 </ul>
 <p>
 <b><code>9999</code></b> : sequential number within the source code, 0001 through
 9999.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_AND_LITERAL">ERRMSG_AND_LITERAL</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_BOGUS_PROOF_LOGHYP_STMT">ERRMSG_BOGUS_PROOF_LOGHYP_STMT</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_DERIV_STEP_PROOF_FAILURE">ERRMSG_DERIV_STEP_PROOF_FAILURE</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_EQUALS_LITERAL">ERRMSG_EQUALS_LITERAL</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_FINAL_STACK_ENTRY_UNEQUAL">ERRMSG_FINAL_STACK_ENTRY_UNEQUAL</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_FINAL_STACK_ENTRY_UNEQUAL2">ERRMSG_FINAL_STACK_ENTRY_UNEQUAL2</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_HYP_TYP_MISMATCH_STACK_TYP">ERRMSG_HYP_TYP_MISMATCH_STACK_TYP</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_LOGHYP_STACK_DEFICIENT">ERRMSG_LOGHYP_STACK_DEFICIENT</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_NO_DERIV_STEPS_CREATED">ERRMSG_NO_DERIV_STEPS_CREATED</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_PROOF_ABS_MAX_RETRY_EXCEEDED">ERRMSG_PROOF_ABS_MAX_RETRY_EXCEEDED</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_PROOF_HAS_ZERO_STEPS">ERRMSG_PROOF_HAS_ZERO_STEPS</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_PROOF_STACK_GT_1_AT_END">ERRMSG_PROOF_STACK_GT_1_AT_END</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_PROOF_STACK_UNDERFLOW">ERRMSG_PROOF_STACK_UNDERFLOW</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_PROOF_STEP_INCOMPLETE">ERRMSG_PROOF_STEP_INCOMPLETE</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_PROOF_STEP_RANGE">ERRMSG_PROOF_STEP_RANGE</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_PSTACK_ARRAY_OVERFLOW">ERRMSG_PSTACK_ARRAY_OVERFLOW</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_RPN_TO_FORMULA_CONV_FAILURE">ERRMSG_RPN_TO_FORMULA_CONV_FAILURE</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_RPN_VERIFY_AS_PROOF_FAILURE">ERRMSG_RPN_VERIFY_AS_PROOF_FAILURE</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_STACK_ITEM_TYP">ERRMSG_STACK_ITEM_TYP</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_STACK_SIZE_MISMATCH_FOR_STEP_HYPS">ERRMSG_STACK_SIZE_MISMATCH_FOR_STEP_HYPS</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_STEP_LOG_HYP_SUBST_UNEQUAL">ERRMSG_STEP_LOG_HYP_SUBST_UNEQUAL</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_SUBST_ARRAY_OVERFLOW">ERRMSG_SUBST_ARRAY_OVERFLOW</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_SUBST_TO_VARS_MATCH">ERRMSG_SUBST_TO_VARS_MATCH</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_SUBST_TO_VARS_NOT_DJ">ERRMSG_SUBST_TO_VARS_NOT_DJ</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_THEOREM_LABEL">ERRMSG_THEOREM_LABEL</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_THEOREM_STEP_LABEL">ERRMSG_THEOREM_STEP_LABEL</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_THEOREM_STEP_NBR">ERRMSG_THEOREM_STEP_NBR</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#ERRMSG_WEXPR_ARRAY_OVERFLOW">ERRMSG_WEXPR_ARRAY_OVERFLOW</a></strong></code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#PROOF_ABSOLUTE_MAX_RETRIES">PROOF_ABSOLUTE_MAX_RETRIES</a></strong></code>
<div class="block">Absolute Maximum Retries!</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#PROOF_PSTACK_HARD_FAILURE_LEN">PROOF_PSTACK_HARD_FAILURE_LEN</a></strong></code>
<div class="block">Proof stack "hard failure" maximum size.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#PROOF_PSTACK_INIT_LEN">PROOF_PSTACK_INIT_LEN</a></strong></code>
<div class="block">Proof stack initial size.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#PROOF_SUBST_HARD_FAILURE_LEN">PROOF_SUBST_HARD_FAILURE_LEN</a></strong></code>
<div class="block">Substitution map array "hard failure" maximum size.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#PROOF_SUBST_INIT_LEN">PROOF_SUBST_INIT_LEN</a></strong></code>
<div class="block">Substitution map array initial size.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#PROOF_WEXPR_HARD_FAILURE_LEN">PROOF_WEXPR_HARD_FAILURE_LEN</a></strong></code>
<div class="block">Work expression (array) "hard failure" maximum size.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#PROOF_WEXPR_INIT_LEN">PROOF_WEXPR_INIT_LEN</a></strong></code>
<div class="block">Work expression (array) initial size.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/ProofConstants.html#QED_STEP_NBR">QED_STEP_NBR</a></strong></code>
<div class="block">QED ProofDerivationStepEntry last step number</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/ProofConstants.html#ProofConstants()">ProofConstants</a></strong>()</code>&nbsp;</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="PROOF_ABSOLUTE_MAX_RETRIES">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>PROOF_ABSOLUTE_MAX_RETRIES</h4>
<pre>public static final&nbsp;int PROOF_ABSOLUTE_MAX_RETRIES</pre>
<div class="block">Absolute Maximum Retries!</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.PROOF_ABSOLUTE_MAX_RETRIES">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="PROOF_PSTACK_INIT_LEN">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>PROOF_PSTACK_INIT_LEN</h4>
<pre>public static final&nbsp;int PROOF_PSTACK_INIT_LEN</pre>
<div class="block">Proof stack initial size.</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.PROOF_PSTACK_INIT_LEN">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="PROOF_PSTACK_HARD_FAILURE_LEN">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>PROOF_PSTACK_HARD_FAILURE_LEN</h4>
<pre>public static final&nbsp;int PROOF_PSTACK_HARD_FAILURE_LEN</pre>
<div class="block">Proof stack "hard failure" maximum size.</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.PROOF_PSTACK_HARD_FAILURE_LEN">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="PROOF_WEXPR_INIT_LEN">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>PROOF_WEXPR_INIT_LEN</h4>
<pre>public static final&nbsp;int PROOF_WEXPR_INIT_LEN</pre>
<div class="block">Work expression (array) initial size.</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.PROOF_WEXPR_INIT_LEN">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="PROOF_WEXPR_HARD_FAILURE_LEN">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>PROOF_WEXPR_HARD_FAILURE_LEN</h4>
<pre>public static final&nbsp;int PROOF_WEXPR_HARD_FAILURE_LEN</pre>
<div class="block">Work expression (array) "hard failure" maximum size.</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.PROOF_WEXPR_HARD_FAILURE_LEN">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="PROOF_SUBST_INIT_LEN">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>PROOF_SUBST_INIT_LEN</h4>
<pre>public static final&nbsp;int PROOF_SUBST_INIT_LEN</pre>
<div class="block">Substitution map array initial size.</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.PROOF_SUBST_INIT_LEN">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="PROOF_SUBST_HARD_FAILURE_LEN">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>PROOF_SUBST_HARD_FAILURE_LEN</h4>
<pre>public static final&nbsp;int PROOF_SUBST_HARD_FAILURE_LEN</pre>
<div class="block">Substitution map array "hard failure" maximum size.</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.PROOF_SUBST_HARD_FAILURE_LEN">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="QED_STEP_NBR">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>QED_STEP_NBR</h4>
<pre>public static final&nbsp;java.lang.String QED_STEP_NBR</pre>
<div class="block">QED ProofDerivationStepEntry last step number</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.QED_STEP_NBR">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_PSTACK_ARRAY_OVERFLOW">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_PSTACK_ARRAY_OVERFLOW</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_PSTACK_ARRAY_OVERFLOW</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_PSTACK_ARRAY_OVERFLOW">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_WEXPR_ARRAY_OVERFLOW">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_WEXPR_ARRAY_OVERFLOW</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_WEXPR_ARRAY_OVERFLOW</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_WEXPR_ARRAY_OVERFLOW">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_SUBST_ARRAY_OVERFLOW">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_SUBST_ARRAY_OVERFLOW</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_SUBST_ARRAY_OVERFLOW</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_SUBST_ARRAY_OVERFLOW">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_PROOF_STEP_INCOMPLETE">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_PROOF_STEP_INCOMPLETE</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_PROOF_STEP_INCOMPLETE</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_PROOF_STEP_INCOMPLETE">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_PROOF_HAS_ZERO_STEPS">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_PROOF_HAS_ZERO_STEPS</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_PROOF_HAS_ZERO_STEPS</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_PROOF_HAS_ZERO_STEPS">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_PROOF_STACK_GT_1_AT_END">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_PROOF_STACK_GT_1_AT_END</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_PROOF_STACK_GT_1_AT_END</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_PROOF_STACK_GT_1_AT_END">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_FINAL_STACK_ENTRY_UNEQUAL">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_FINAL_STACK_ENTRY_UNEQUAL</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_FINAL_STACK_ENTRY_UNEQUAL</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_FINAL_STACK_ENTRY_UNEQUAL">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_THEOREM_LABEL">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_THEOREM_LABEL</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_THEOREM_LABEL</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_THEOREM_LABEL">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_THEOREM_STEP_NBR">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_THEOREM_STEP_NBR</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_THEOREM_STEP_NBR</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_THEOREM_STEP_NBR">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_THEOREM_STEP_LABEL">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_THEOREM_STEP_LABEL</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_THEOREM_STEP_LABEL</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_THEOREM_STEP_LABEL">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_HYP_TYP_MISMATCH_STACK_TYP">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_HYP_TYP_MISMATCH_STACK_TYP</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_HYP_TYP_MISMATCH_STACK_TYP</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_HYP_TYP_MISMATCH_STACK_TYP">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_STACK_ITEM_TYP">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_STACK_ITEM_TYP</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_STACK_ITEM_TYP</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_STACK_ITEM_TYP">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_SUBST_TO_VARS_MATCH">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_SUBST_TO_VARS_MATCH</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_SUBST_TO_VARS_MATCH</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_SUBST_TO_VARS_MATCH">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_SUBST_TO_VARS_NOT_DJ">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_SUBST_TO_VARS_NOT_DJ</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_SUBST_TO_VARS_NOT_DJ</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_SUBST_TO_VARS_NOT_DJ">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_STEP_LOG_HYP_SUBST_UNEQUAL">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_STEP_LOG_HYP_SUBST_UNEQUAL</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_STEP_LOG_HYP_SUBST_UNEQUAL</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_STEP_LOG_HYP_SUBST_UNEQUAL">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_RPN_VERIFY_AS_PROOF_FAILURE">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_RPN_VERIFY_AS_PROOF_FAILURE</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_RPN_VERIFY_AS_PROOF_FAILURE</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_RPN_VERIFY_AS_PROOF_FAILURE">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_PROOF_STACK_UNDERFLOW">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_PROOF_STACK_UNDERFLOW</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_PROOF_STACK_UNDERFLOW</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_PROOF_STACK_UNDERFLOW">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_EQUALS_LITERAL">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_EQUALS_LITERAL</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_EQUALS_LITERAL</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_EQUALS_LITERAL">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_AND_LITERAL">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_AND_LITERAL</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_AND_LITERAL</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_AND_LITERAL">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_PROOF_ABS_MAX_RETRY_EXCEEDED">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_PROOF_ABS_MAX_RETRY_EXCEEDED</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_PROOF_ABS_MAX_RETRY_EXCEEDED</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_PROOF_ABS_MAX_RETRY_EXCEEDED">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_DERIV_STEP_PROOF_FAILURE">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_DERIV_STEP_PROOF_FAILURE</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_DERIV_STEP_PROOF_FAILURE</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_DERIV_STEP_PROOF_FAILURE">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_RPN_TO_FORMULA_CONV_FAILURE">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_RPN_TO_FORMULA_CONV_FAILURE</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_RPN_TO_FORMULA_CONV_FAILURE</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_RPN_TO_FORMULA_CONV_FAILURE">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_BOGUS_PROOF_LOGHYP_STMT">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_BOGUS_PROOF_LOGHYP_STMT</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_BOGUS_PROOF_LOGHYP_STMT</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_BOGUS_PROOF_LOGHYP_STMT">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_LOGHYP_STACK_DEFICIENT">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_LOGHYP_STACK_DEFICIENT</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_LOGHYP_STACK_DEFICIENT</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_LOGHYP_STACK_DEFICIENT">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_FINAL_STACK_ENTRY_UNEQUAL2">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_FINAL_STACK_ENTRY_UNEQUAL2</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_FINAL_STACK_ENTRY_UNEQUAL2</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_FINAL_STACK_ENTRY_UNEQUAL2">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_NO_DERIV_STEPS_CREATED">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_NO_DERIV_STEPS_CREATED</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_NO_DERIV_STEPS_CREATED</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_NO_DERIV_STEPS_CREATED">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_STACK_SIZE_MISMATCH_FOR_STEP_HYPS">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ERRMSG_STACK_SIZE_MISMATCH_FOR_STEP_HYPS</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_STACK_SIZE_MISMATCH_FOR_STEP_HYPS</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_STACK_SIZE_MISMATCH_FOR_STEP_HYPS">Constant Field Values</a></dd></dl>
</li>
</ul>
<a name="ERRMSG_PROOF_STEP_RANGE">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>ERRMSG_PROOF_STEP_RANGE</h4>
<pre>public static final&nbsp;java.lang.String ERRMSG_PROOF_STEP_RANGE</pre>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../constant-values.html#mmj.verify.ProofConstants.ERRMSG_PROOF_STEP_RANGE">Constant Field Values</a></dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="ProofConstants()">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>ProofConstants</h4>
<pre>public&nbsp;ProofConstants()</pre>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/NullsPermittedRule.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/verify/ProofDerivationStepEntry.html" title="class in mmj.verify"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/ProofConstants.html" target="_top">Frames</a></li>
<li><a href="ProofConstants.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#methods_inherited_from_class_java.lang.Object">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li>Method</li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
